YES 12.259 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((group :: [Int ->  [[Int]]) :: [Int ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a ->  [[a]]
group groupBy (==)

  groupBy :: (a  ->  a  ->  Bool ->  [a ->  [[a]]
groupBy [] []
groupBy eq (x : xs
(x : ys: groupBy eq zs where 
vv10 span (eq x) xs
ys (\(ys,_) ->ys) vv10
zs (\(_,zs) ->zs) vv10


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys

The following Lambda expression
\(_,zs)→zs

is transformed to
zs1 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys1 (ys,_) = ys



↳ HASKELL
  ↳ LR
HASKELL
      ↳ BR

mainModule List
  ((group :: [Int ->  [[Int]]) :: [Int ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a ->  [[a]]
group groupBy (==)

  groupBy :: (a  ->  a  ->  Bool ->  [a ->  [[a]]
groupBy [] []
groupBy eq (x : xs
(x : ys: groupBy eq zs where 
vv10 span (eq x) xs
ys ys0 vv10
ys0 (ys,_) ys
zs zs0 vv10
zs0 (_,zszs


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule List
  ((group :: [Int ->  [[Int]]) :: [Int ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a ->  [[a]]
group groupBy (==)

  groupBy :: (a  ->  a  ->  Bool ->  [a ->  [[a]]
groupBy vw [] []
groupBy eq (x : xs
(x : ys: groupBy eq zs where 
vv10 span (eq x) xs
ys ys0 vv10
ys0 (ys,vxys
zs zs0 vv10
zs0 (vy,zszs


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

span3 p [] = ([],[])
span3 xx xy = span2 xx xy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ LetRed

mainModule List
  ((group :: [Int ->  [[Int]]) :: [Int ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a ->  [[a]]
group groupBy (==)

  groupBy :: (a  ->  a  ->  Bool ->  [a ->  [[a]]
groupBy vw [] []
groupBy eq (x : xs
(x : ys: groupBy eq zs where 
vv10 span (eq x) xs
ys ys0 vv10
ys0 (ys,vxys
zs zs0 vv10
zs0 (vy,zszs


module Maybe where
  import qualified List
import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
(x : ys: groupBy eq zs
where 
vv10  = span (eq xxs
ys  = ys0 vv10
ys0 (ys,vx) = ys
zs  = zs0 vv10
zs0 (vy,zs) = zs

are unpacked to the following functions on top level
groupByYs0 xz yu yv (ys,vx) = ys

groupByZs0 xz yu yv (vy,zs) = zs

groupByYs xz yu yv = groupByYs0 xz yu yv (groupByVv10 xz yu yv)

groupByVv10 xz yu yv = span (xz yuyv

groupByZs xz yu yv = groupByZs0 xz yu yv (groupByVv10 xz yu yv)

The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

are unpacked to the following functions on top level
span2Ys yw yx = span2Ys1 yw yx (span2Vu43 yw yx)

span2Zs yw yx = span2Zs1 yw yx (span2Vu43 yw yx)

span2Zs1 yw yx (wy,zs) = zs

span2Span0 yw yx p ww wx True = ([],ww : wx)

span2Span1 yw yx p ww wx True = (ww : span2Ys yw yx,span2Zs yw yx)
span2Span1 yw yx p ww wx False = span2Span0 yw yx p ww wx otherwise

span2Vu43 yw yx = span yw yx

span2Ys1 yw yx (ys,wz) = ys



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
HASKELL
                  ↳ Narrow

mainModule List
  (group :: [Int ->  [[Int]])

module List where
  import qualified Maybe
import qualified Prelude

  group :: Eq a => [a ->  [[a]]
group groupBy (==)

  groupBy :: (a  ->  a  ->  Bool ->  [a ->  [[a]]
groupBy vw [] []
groupBy eq (x : xs(x : groupByYs eq x xs: groupBy eq (groupByZs eq x xs)

  
groupByVv10 xz yu yv span (xz yu) yv

  
groupByYs xz yu yv groupByYs0 xz yu yv (groupByVv10 xz yu yv)

  
groupByYs0 xz yu yv (ys,vxys

  
groupByZs xz yu yv groupByZs0 xz yu yv (groupByVv10 xz yu yv)

  
groupByZs0 xz yu yv (vy,zszs


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Zs0(yy376, yy378)
new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Zs0(yy370, yy372)
new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Ys0(yy376, yy378)
new_span2Zs0(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs1(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys0(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys1(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs1(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs1(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Ys0(yy370, yy372)
new_span2Ys1(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys1(yy370, yy371, yy372, yy3730, yy3740)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByZs0(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs0(yy189, yy190, yy191, yy1920, yy1930)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByYs0(yy142, yy143, yy144, Succ(yy1450), Succ(yy1460)) → new_groupByYs0(yy142, yy143, yy144, yy1450, yy1460)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Zs3(yy358, yy360)
new_span2Ys3(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys10(yy69, yy71000, yy711, yy69, yy71000)
new_span2Zs3(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs10(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Ys3(yy364, yy366)
new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Zs3(yy364, yy366)
new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Ys3(yy358, yy360)
new_span2Zs10(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs10(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys10(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys10(yy358, yy359, yy360, yy3610, yy3620)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByZs00(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs00(yy183, yy184, yy185, yy1860, yy1870)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_groupByYs00(yy136, yy137, yy138, Succ(yy1390), Succ(yy1400)) → new_groupByYs00(yy136, yy137, yy138, yy1390, yy1400)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_groupBy(:(yy30, yy31)) → new_groupBy(new_groupByZs01(yy30, yy31))

The TRS R consists of the following rules:

new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys6(yy69, []) → []
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs110(yy3111, yy17, yy16) → yy16
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_groupByZs01(yy30, []) → []
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs5([]) → []
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys5([]) → []
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_span2Zs7([]) → []
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys4(yy66, []) → []
new_span2Ys7([]) → []
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_span2Zs4(yy82, []) → []
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys14(yy370, yy371, yy372) → []
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)

The set Q consists of the following terms:

new_span2Zs15(x0, x1, x2)
new_span2Zs7([])
new_span2Zs14(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys17(x0, x1, x2, Zero, Succ(x3))
new_span2Ys6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys12(x0, x1, x2)
new_span2Zs4(x0, [])
new_span2Zs18(x0, x1, x2)
new_span2Zs11(x0, x1, x2, Zero, Succ(x3))
new_span2Zs110(x0, x1, x2)
new_span2Zs7(:(Pos(Succ(x0)), x1))
new_span2Ys14(x0, x1, x2)
new_span2Zs5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Succ(x3), Zero)
new_span2Ys5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Zero, Zero)
new_span2Zs19(x0, x1, x2, x3, x4)
new_span2Ys7([])
new_span2Ys11(x0, x1, x2)
new_groupByZs01(Pos(Zero), :(Pos(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Succ(x3))
new_span2Zs7(:(Neg(Zero), x0))
new_span2Zs14(x0, x1, x2, Succ(x3), Zero)
new_span2Ys110(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Zero), :(Pos(Zero), x0))
new_groupByZs07(x0, x1, x2, x3, x4)
new_span2Zs5(:(Neg(Succ(x0)), x1))
new_groupByZs02(x0, x1, x2)
new_span2Ys7(:(Pos(Succ(x0)), x1))
new_span2Ys4(x0, :(Pos(x1), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Neg(Zero), x0))
new_span2Zs13(x0, x1, x2, x3, x4)
new_span2Ys16(x0, x1, x2, x3, x4)
new_span2Zs4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys7(:(Neg(Succ(x0)), x1))
new_span2Ys7(:(Neg(Zero), x0))
new_span2Ys17(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Succ(x0)), :(Pos(x1), x2))
new_groupByZs01(Neg(Succ(x0)), :(Neg(Succ(x1)), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Succ(x4))
new_groupByZs05(x0, x1, x2, Zero, Succ(x3))
new_span2Ys5(:(Neg(Zero), x0))
new_span2Ys19(x0, x1, x2)
new_span2Zs5(:(Pos(Zero), x0))
new_groupByZs01(Pos(Succ(x0)), :(Pos(Zero), x1))
new_groupByZs05(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys4(x0, :(Neg(Zero), x1))
new_span2Ys5(:(Neg(Succ(x0)), x1))
new_groupByZs01(Neg(Zero), :(Neg(Succ(x0)), x1))
new_span2Ys6(x0, [])
new_groupByZs01(Neg(Succ(x0)), :(Neg(Zero), x1))
new_span2Ys6(x0, :(Neg(x1), x2))
new_span2Zs12(x0, x1, x2)
new_groupByZs01(Neg(Zero), :(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Zero)
new_span2Zs11(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs16(x0, x1, x2)
new_span2Ys5(:(Pos(Zero), x0))
new_span2Ys6(x0, :(Pos(Zero), x1))
new_span2Zs17(x0, x1, x2)
new_span2Ys4(x0, [])
new_groupByZs01(x0, [])
new_span2Zs4(x0, :(Pos(x1), x2))
new_span2Zs6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys13(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys5([])
new_span2Zs6(x0, [])
new_span2Ys7(:(Pos(Zero), x0))
new_span2Ys17(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Neg(Zero), :(Pos(Succ(x0)), x1))
new_span2Ys17(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs4(x0, :(Neg(Zero), x1))
new_groupByZs06(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Succ(x0)), :(Neg(x1), x2))
new_span2Zs14(x0, x1, x2, Zero, Succ(x3))
new_groupByZs01(Pos(Zero), :(Neg(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Zero)
new_span2Ys13(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Pos(Zero), x0))
new_span2Zs5([])
new_span2Zs7(:(Pos(Zero), x0))
new_span2Ys15(x0, x1, x2, x3, x4)
new_groupByZs01(Pos(Succ(x0)), :(Pos(Succ(x1)), x2))
new_span2Zs14(x0, x1, x2, Zero, Zero)
new_groupByZs04(x0, x1, x2, x3, x4)
new_span2Zs6(x0, :(Pos(Zero), x1))
new_span2Zs6(x0, :(Neg(x1), x2))
new_span2Ys4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys18(x0, x1, x2)
new_span2Zs7(:(Neg(Succ(x0)), x1))
new_span2Zs5(:(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Succ(x3))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_groupBy(:(yy30, yy31)) → new_groupBy(new_groupByZs01(yy30, yy31))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x1, x2)) = 1 + x2   
POL(Neg(x1)) = 0   
POL(Pos(x1)) = 0   
POL(Succ(x1)) = 0   
POL(Zero) = 0   
POL([]) = 0   
POL(new_groupBy(x1)) = x1   
POL(new_groupByZs01(x1, x2)) = x2   
POL(new_groupByZs02(x1, x2, x3)) = 1 + x3   
POL(new_groupByZs03(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_groupByZs04(x1, x2, x3, x4, x5)) = x5   
POL(new_groupByZs05(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_groupByZs06(x1, x2, x3)) = 1 + x3   
POL(new_groupByZs07(x1, x2, x3, x4, x5)) = x5   
POL(new_span2Ys11(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys110(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys12(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys13(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Ys14(x1, x2, x3)) = 0   
POL(new_span2Ys15(x1, x2, x3, x4, x5)) = 1 + x4   
POL(new_span2Ys16(x1, x2, x3, x4, x5)) = 1 + x4   
POL(new_span2Ys17(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Ys18(x1, x2, x3)) = 0   
POL(new_span2Ys19(x1, x2, x3)) = 1 + x2   
POL(new_span2Ys4(x1, x2)) = x2   
POL(new_span2Ys5(x1)) = x1   
POL(new_span2Ys6(x1, x2)) = x2   
POL(new_span2Ys7(x1)) = x1   
POL(new_span2Zs11(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Zs110(x1, x2, x3)) = x3   
POL(new_span2Zs12(x1, x2, x3)) = 1 + x3   
POL(new_span2Zs13(x1, x2, x3, x4, x5)) = 1 + x5   
POL(new_span2Zs14(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Zs15(x1, x2, x3)) = x3   
POL(new_span2Zs16(x1, x2, x3)) = x3   
POL(new_span2Zs17(x1, x2, x3)) = 1 + x3   
POL(new_span2Zs18(x1, x2, x3)) = 1 + x3   
POL(new_span2Zs19(x1, x2, x3, x4, x5)) = x5   
POL(new_span2Zs4(x1, x2)) = x2   
POL(new_span2Zs5(x1)) = x1   
POL(new_span2Zs6(x1, x2)) = x2   
POL(new_span2Zs7(x1)) = x1   

The following usable rules [17] were oriented:

new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Ys4(yy66, []) → []
new_groupByZs01(yy30, []) → []
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys14(yy370, yy371, yy372) → []
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5([]) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys6(yy69, []) → []
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys5([]) → []
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Ys7([]) → []
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs7([]) → []
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Zs4(yy82, []) → []
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs110(yy3111, yy17, yy16) → yy16



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof
QDP
                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys6(yy69, []) → []
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs110(yy3111, yy17, yy16) → yy16
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_groupByZs01(yy30, []) → []
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs5([]) → []
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys5([]) → []
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_span2Zs7([]) → []
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys4(yy66, []) → []
new_span2Ys7([]) → []
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_span2Zs4(yy82, []) → []
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys14(yy370, yy371, yy372) → []
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)

The set Q consists of the following terms:

new_span2Zs15(x0, x1, x2)
new_span2Zs7([])
new_span2Zs14(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys17(x0, x1, x2, Zero, Succ(x3))
new_span2Ys6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys12(x0, x1, x2)
new_span2Zs4(x0, [])
new_span2Zs18(x0, x1, x2)
new_span2Zs11(x0, x1, x2, Zero, Succ(x3))
new_span2Zs110(x0, x1, x2)
new_span2Zs7(:(Pos(Succ(x0)), x1))
new_span2Ys14(x0, x1, x2)
new_span2Zs5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Succ(x3), Zero)
new_span2Ys5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Zero, Zero)
new_span2Zs19(x0, x1, x2, x3, x4)
new_span2Ys7([])
new_span2Ys11(x0, x1, x2)
new_groupByZs01(Pos(Zero), :(Pos(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Succ(x3))
new_span2Zs7(:(Neg(Zero), x0))
new_span2Zs14(x0, x1, x2, Succ(x3), Zero)
new_span2Ys110(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Zero), :(Pos(Zero), x0))
new_groupByZs07(x0, x1, x2, x3, x4)
new_span2Zs5(:(Neg(Succ(x0)), x1))
new_groupByZs02(x0, x1, x2)
new_span2Ys7(:(Pos(Succ(x0)), x1))
new_span2Ys4(x0, :(Pos(x1), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Neg(Zero), x0))
new_span2Zs13(x0, x1, x2, x3, x4)
new_span2Ys16(x0, x1, x2, x3, x4)
new_span2Zs4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys7(:(Neg(Succ(x0)), x1))
new_span2Ys7(:(Neg(Zero), x0))
new_span2Ys17(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Succ(x0)), :(Pos(x1), x2))
new_groupByZs01(Neg(Succ(x0)), :(Neg(Succ(x1)), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Succ(x4))
new_groupByZs05(x0, x1, x2, Zero, Succ(x3))
new_span2Ys5(:(Neg(Zero), x0))
new_span2Ys19(x0, x1, x2)
new_span2Zs5(:(Pos(Zero), x0))
new_groupByZs01(Pos(Succ(x0)), :(Pos(Zero), x1))
new_groupByZs05(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys4(x0, :(Neg(Zero), x1))
new_span2Ys5(:(Neg(Succ(x0)), x1))
new_groupByZs01(Neg(Zero), :(Neg(Succ(x0)), x1))
new_span2Ys6(x0, [])
new_groupByZs01(Neg(Succ(x0)), :(Neg(Zero), x1))
new_span2Ys6(x0, :(Neg(x1), x2))
new_span2Zs12(x0, x1, x2)
new_groupByZs01(Neg(Zero), :(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Zero)
new_span2Zs11(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs16(x0, x1, x2)
new_span2Ys5(:(Pos(Zero), x0))
new_span2Ys6(x0, :(Pos(Zero), x1))
new_span2Zs17(x0, x1, x2)
new_span2Ys4(x0, [])
new_groupByZs01(x0, [])
new_span2Zs4(x0, :(Pos(x1), x2))
new_span2Zs6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys13(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys5([])
new_span2Zs6(x0, [])
new_span2Ys7(:(Pos(Zero), x0))
new_span2Ys17(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Neg(Zero), :(Pos(Succ(x0)), x1))
new_span2Ys17(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs4(x0, :(Neg(Zero), x1))
new_groupByZs06(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Succ(x0)), :(Neg(x1), x2))
new_span2Zs14(x0, x1, x2, Zero, Succ(x3))
new_groupByZs01(Pos(Zero), :(Neg(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Zero)
new_span2Ys13(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Pos(Zero), x0))
new_span2Zs5([])
new_span2Zs7(:(Pos(Zero), x0))
new_span2Ys15(x0, x1, x2, x3, x4)
new_groupByZs01(Pos(Succ(x0)), :(Pos(Succ(x1)), x2))
new_span2Zs14(x0, x1, x2, Zero, Zero)
new_groupByZs04(x0, x1, x2, x3, x4)
new_span2Zs6(x0, :(Pos(Zero), x1))
new_span2Zs6(x0, :(Neg(x1), x2))
new_span2Ys4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys18(x0, x1, x2)
new_span2Zs7(:(Neg(Succ(x0)), x1))
new_span2Zs5(:(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Succ(x3))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.